$\forall$${\it es}$:event\_system\{i:l\}, $e$,$a$:es{-}E(${\it es}$).
\\[0ex]es{-}locl(${\it es}$; $a$; $e$)
\\[0ex]$\Rightarrow$ ($\exists$$b$:es{-}E(${\it es}$). (($\neg$($\uparrow$es{-}first(${\it es}$; $b$))) c$\wedge$ (($a$ = es{-}pred(${\it es}$; $b$)) $\wedge$ es{-}le(${\it es}$; $b$; $e$))))